\section{Characterizing uncertainty in transformations}\label{sec:incompleteness}
\noindent

\begin{comment}{Content}
In this section, we will provide a formal / rigorous characterization of bidirection transformations with uncertainty. Possibly, under which conditions transformations can produce non-determinism.
\end{comment}


As any other software artifact, uncertainty affects bidirectional transformations. As showed in the previous scenario, when modelers are not able to fix a decision may encode ambiguities in their model transformation specification (e.g. not providing additional constraints that would make the transformation deterministic) such that more design alternatives are maintained during the modeling process.

Most of the current unidirectional languages consider transformations as \emph{one-to-one} functions, in contrast to bidirectional transformations which involve \emph{one-to-many} cardinality. In this case, intrinsic characteristics of model transformations influence the effect of uncertain information. 
%More formally, a bidirectional transformation is defined as a consistency relation $C$ between a left-model $M^{L} \in MM^{L}$ and a right-model $M^{R}\in MM^{R}$, denoted by $M^{L} C M^{R}$. Let us to consider the following properties: 
%\begin{itemize}
%\item[1)] $C$ can be \emph{left-total}, when for every left-model $M^{L}$, there exists at least one right-model $M^{R}$ such that $M^{L} C M^{R}$; and \emph{right-total}, which is the dual and defined analogously;
%\item[2)] $C$ can be \emph{left-unique}, when for every right-model
%$M^{R}$, there exists at most one left model $M^{L}$ such that $M^{L} C M^{R}$; and \emph{right-unique}, which is the dual and defined analogously\footnote{In order to clarify the used terms: a left-total relation is also called \emph{total}, right-total \emph{surjective}, left-unique \emph{injective}, and right-unique \emph{functional}.};
%\end{itemize}
Let us to consider a bidirectional transformation defined as a consistency relation $R(M_{S},M_{T})$ between a source model $M_{S} \in MM_{S}$ and a target model $M_{T}\in MM_{T}$;
%By adapting well consolidate mathematical properties, let us to consider the following totality properties: 
by adapting well consolidated mathematical concepts, we obtain \emph{totality} and \emph{uniqueness} properties, as following: 

\noindent
{\bf Uniqueness.} The designer may write \emph{non-unique} transformations writing a not univocal mapping with a one-to-many cardinality. In this case, during the execution, more than one model corresponds to a given one. This situation arises especially in cases in which the involved meta-models \emph{not isomorphic}. In particular, 
\begin{itemize}
\item[-] $R$ is a \emph{functional} relation if for all source model $M_{S}$ there exists at most one target model $M_{T}$ such that $R(M_{S},M_{T})$
\item[-] $R$ is a \emph{injective} relation if for all target model $M_{T}$ there exists at most one source model $M_{S}$ such that $R(M_{S},M_{T})$
\end{itemize}
{\bf Totality.}  The lack of information can lead designers to writing \emph{non-total} mappings (i.e., not all the elements of the domain are mapped in correspondent elements of the co-domain), designers who need to express their uncertainty write total relations. In particular, 
\begin{itemize}
\item[-] $R$ is a \emph{total} relation if for all source model $M_{S}$ there exists at least one target model $M_{T}$ such that $R(M_{S},M_{T})$
\item[-] $R$ is a \emph{surjective} relation if for all target model $M_{T}$ there exists at least one source model $M_{S}$ such that $R(M_{S},M_{T})$
\end{itemize}



%Uniqueness properties:
%injective (also called left-unique[5]): for all x and z in X and y in Y it holds that if xRy and zRy then x = z. For example, the green relation in the picture is injective, but the red relation is not, as it relates e.g. both x=-5 and z=+5 to y=25.
%
%functional (also called univalent[6] or right-unique[5] or right-definite[citation needed]): for all x in X, and y and z in Y it holds that if xRy and xRz then y = z; such a binary relation is called a partial function. Both relations in the picture are functional. An example for a non-functional relation can be obtained by rotating the red graph clockwise by 90 degrees, i.e. by considering the relation x=y2 which relates e.g. x=25 to both y=-5 and z=+5.
%one-to-one (also written 1-to-1): injective and functional. The green relation is one-to-one, but the red is not.
%Totality properties:
%left-total:[5] for all x  there exists a y in Y such that xRy, i.e., R is a multivalued function (this property, although sometimes also referred to as total, is different from the definition of total in the next section). Both relations in the picture are left-total. The relation x=y2, obtained from the above rotation, is not left-total, as it doesn't relate, e.g., x=-14 to any real number y.
%surjective (also called right-total[5] or onto): for all y there exists an x  such that xRy. The green relation is surjective, but the red relation is not, as it doesn't relate any real number x to e.g. y=-14.
%Uniqueness and totality properties:
%A function: a relation that is functional and left-total. Both the green and the red relation are functions.
%A bijection: a surjective one-to-one or surjective injective function is said to be bijective, also known as one-to-one correspondence.[7] The green relation is bijective, but the red is not.

\noindent
These features are used to characterize a bidirectional transformation which encode the designer uncertainty and give the conditions under which its execution generates uncertainty, i.e. different design alternatives as outcome. In particular, %coupled with the other is cause of uncertainty in generated models that represents multiple design solutions. 
\vspace{0,3cm}

\noindent
{\bf Uncertain transformation.}  Considering a bidirectional transformation $R$ as two directional functions:
 
\vspace{0,1cm}
$\overrightarrow{R} : M_S \times M_T \rightarrow M_T$, 

\vspace{0,05cm}
$\overleftarrow{R} : M_S \times M_T \rightarrow M_S$,
\vspace{0,1cm}

\noindent
$\overrightarrow{R}$ \emph{generates uncertainty} if it is a non-functional and total relation, whereas $\overleftarrow{R}$ \emph{generates uncertainty} if is a non-injective and surjective relation.

%Given the forward transformation $\overrightarrow{R} : M_S \times M_T \rightarrow M_T$, $\overrightarrow{R}$ contains uncertainty if is a non-injective and total relation.
%
%Given the backward transformation $\overleftarrow{R} : M_S \times M_T \rightarrow M_T$, $\overrightarrow{R}$ contains uncertainty if is a non-injective and total relation.
%
%In this respect, we define that: 
%\begin{itemize}
%\item[-] $R$ is a \emph{forward under-specified} relation if is a non-injective and total relation
%\item[-] $R$ is a \emph{backward under-specified} relation if is a non-functional and surjective relation
%\end{itemize}

\vspace{0,3cm}

{\bf Qui sotto descrivo come si comportano gli approcci correnti e che ci sono difficoltà nel trattare con uncertainty. Motivo la scelta di JTL.}

Current bidirectional transformation languages typically deal with non-de\-ter\-mi\-ni\-sm by requiring the mapping to fix ambiguities by adding additional constraints, which have to be known beforehand the transformation implementation. 
In this case, inconsistencies are solved by means of choices that a designer must take when writing a transformation. Choices may be a consequences of different ways to write transformations, but it is important to consider that some application domains or some particular phase of the software development prevent designers from encoding their decision within the transformation code.
In this cases, the designer need to specify ambiguous mappings and to postpone her decisions in later stages. For this purpose, a technique able to deal with non-determinism and to generate all the valid design alternatives can be adopted. Therefore, this is not a drawback but rather a requirements for express designer indecision.  
For the reasons introduced in this Section, in this work we consider the Janus Transformation Language (JTL)~\cite{CDEP10}, a bidirectional model transformation language able to deal with non-deterministic cases by generating multiple alternatives as outcome of the transformation execution. Next Section introduces JTL and shows how it is able to deal with uncertainty and multiple design solutions.  


\section{Case Study: JTL}\label{sec:jtl}

%pezzo da mise
%Most of the current bidirectional languages have difficulties in dealing with problems as those described above. More recently, few language-centric approaches~\cite{CDEP10,MC13,CK13} have been proposed in order to give a more rigorous support to non-bijectivity in transformations, even though each has its own flavor (see Sect.~\ref{sec:related} for a discussion). In this paper, we consider the Janus Transformation Language (JTL)~\cite{CDEP10}, a bidirectional model transformation language able to deal with non-deterministic cases by generating multiple alternatives as outcome of the transformation execution. Next Section introduces JTL and shows how it is able to deal with uncertainty.  


\subsection{An overview of JTL} \label{sec:jtl-overview}
JTL is a constraint-based model transformation language specifically tailored to support bidirectionality. It adopts a QVT-R \cite{QVT-Final} like syntax and allows a declarative specification of relationships between MOF models. The language supports object pattern matching, and implicitly creates trace instances to record what occurred during a transformation execution. 

The semantics is given in terms of Answer Set Programming (ASP) \cite{GL88}, which is a form of declarative programming oriented towards difficult (primarily NP-hard) search problems and based on the stable model (answer set) semantics of logic programming.
In particular, the \emph{transformation engine} consists of bidirectional rules able to interpret the correspondences among elements and execute the transformation. 
Then the ASP solver~\footnote{http://www.dlvsystem.com/} finds and generates, in a single execution, all the possible models which are consistent with the transformation rules by a deductive process. 

The JTL environment has been implemented as a set of plug-ins of the Eclipse framework and mainly exploits %the Eclipse Modelling Framework (EMF)
EMF \footnote{http://www.eclipse.org/modeling/emf/}. It allows the designer to specify bidirectional transformations in the JTL syntax and to manipulate models and metamodels in their EMF format, making the ASP semantics totally transparent.


%\vspace{-0.15cm}
\subsection{Specifying transformations}\label{sec:jtl-spec}
\noindent
In this Section we illustrate how it is possible to specify incomplete model transformations such that uncertainty is generated. In Listing~\ref{lst:HSM2SMtransfJTL} we report a fragment of the \emph{HSM2SM} transformation which maps hierarchical state machines into flat state machines and the other way round. A transformation between candidate models is specified as a set of \emph{relation}s defined by two \emph{domain}s
%(like \emph{State2State} specified in lines \emph{6-10}) 
that must hold for the transformation to be successful. In particular, in Listing ~\ref{lst:HSM2SMtransfJTL} the following relations are defined: 
%a) \emph{StateMachine2StateMachine} which relates state machines of the hierarchical metamodel and state machines of the flat metamodel,  
%b) \emph{State2State} which relates states of the hierarchical metamodel and states of the flat metamodel,  
%c) \emph{CompositeState2State} which relates composite states of the hierarchical metamodel and states of the flat metamodel, 
a) \emph{Transition2Transition} which relates transitions  of the hierarchical metamodel and transitions of the flat metamodel,
b) \emph{TransitionSource2TransitionSource} which relates source states of transitions of the hierarchical metamodel and the corespondent source states of transitions of the flat metamodel, and c) \emph{TransitionSourceComposite2TransitionSource} which relates source composite states of transitions of the hierarchical metamodel and correspondent source states of transitions of the flat metamodel\footnote{ %For the sake of readability, the relations involving the target state of transitions are left out. However, the interest reader can access the full implementation at
The full implementation is available at http://jtl.di.univaq.it/}.
Each relation includes a pair of \emph{when} and \emph{where} predicates which specify the pre- and post- conditions that must be satisfied by the elements of the candidate models. %For instance, the when clause in lines \code{18-21} implies that the \emph{State2State} relation is satisfied only if the \emph{StateMachine2StateMachine} relation is satisfied and the considered source state is an atomic states. 
A transformation can be invoked for \emph{enforcement} or as \emph{checkonly}. When invoked for enforcement, it is executed in a particular direction by selecting one of the candidate models as the target. 
A transformation can also be invoked in bidirectional mode (as in Listing~\ref{lst:HSM2SMtransfJTL}) by marking as enforcement both domain directions.

The transformation is clearly non-injective as many different hierarchical machines can be flattened to the same model and consequently transforming a flat machine can give place to more than one hierarchical machine. In the example depicted in Figure \ref{fig:stateMachines}, 
%the back propagation of changes gives place to uncertainty. As,  interesting situation: 
the new \code{print} transition can be equally mapped to each one of the nested states within \code{Active} as well as to the container state itself. In fact, considering the \emph{HSM2SM} transformation in Listing~\ref{lst:HSM2SMtransfJTL}, the \emph{TransitionSource2TransitionSource} and \emph{TransitionSource2TransitionSour\-ce} relations are satisfied in equal way and no further condition is added in order to fix the behavior. As a consequence, more than one valid alternative may be proposed as output of the transformation, leaving the designers with a choice of suitable solutions. 

%top relation StateMachine2StateMachine {
%		enforce domain source sSM: HSM::StateMachine { };
%		enforce domain target tSM: SM::StateMachine { };
%	}
%	
%	top relation State2State {
%		varName : String;
%		enforce domain source sourceState: HSM::State {
%			owningStateMachine = sourceSM: HSM::StateMachine { },
%			name = varName
%		};
%		enforce domain target targetState: SM::State {
%			owningStateMachine = targetSM: SM::StateMachine { },
%			name = varName
%		};
%		when {
%			StateMachine2StateMachine(sourceSM, targetSM) and 
%			not sourceState.owningCompositeState.oclIsUndefined();
%		}
%	}
%    
%	top relation CompositeState2State {
%		varName : String;
%		enforce domain source sourceState: HSM::CompositeState{
%			owningStateMachine = sourceSM: HSM::StateMachine {	},
%			name = varName
%		};
%		enforce domain target targetState: SM::State {
%			owningStateMachine = targetSM: SM::StateMachine { },
%			name = varName
%		};
%		when { StateMachine2StateMachine(sourceSM, targetSM); }
%	}
%abovecaptionskip=-0.6cm, aboveskip=0.2cm,
\begin{lstlisting}[breaklines,style=AMMA,language=ASPencoding,mathescape,rulesepcolor=\color{black},caption={ A fragment of the HSM2SM transformation in JTL},captionpos=b, aboveskip=0.5cm, belowskip=0.5cm, label={lst:HSM2SMtransfJTL}]
transformation hsm2sm(source : HSM, target : SM) {
	...
	top relation Transition2Transition {
		enforce domain source sourceTrans: HSM::Transition{
			owningStateMachine = sourceSM: HSM::StateMachine { },
		};
		enforce domain target targetTrans: SM::Transition{
			owningStateMachine = targetSM: SM::StateMachine { },
		};
		when {...}
		where {...}
	}
	relation TransitionSource2TransitionSource {
		enforce domain source sourceTrans: HSM::Transition {
			source = sourceState : HSM::State { }
		};
		enforce domain target targetTrans: SM::Transition {
			source = targetState : SM::State { }
		};
		when {
			State2State(sourceState, targetState) and 
			sourceState.owningCompositeState.oclIsUndefined();
		}
	}
	relation TransitionSourceComposite2TransitionSource {
		enforce domain source sourceTrans: HSM::Transition {
			source = sourceState : HSM::CompositeState { }
		};
		enforce domain target targetTrans: SM::Transition {
			source = targetState : SM::State { }
		};
		when { 
			CompositeState2State(sourceState, targetState);
		}	
	}  
    ...
}           
\end{lstlisting}
%\vspace{-0.2cm}

 \begin{figure}[ht]
   \center
    \includegraphics[width=8.5cm]{figures/xmi_a_b-new.jpg}
    %\vspace{-0.6cm}
    \caption{The HSM model and the correspondent SM model}
    %\vspace{-0.2cm}
      \label{fig:HSM2SMmodels}
 \end{figure}
 	
\subsection{Generating the solution space}\label{sec:jtl-gen}
\noindent
The transformation execution and the generation of the solutions is delegated to the JTL transformation engine implemented in ASP. In particular, it is able to interpret the correspondences among element types (\emph{relations}) and the restrictions on the given relations (\emph{constraints}) and execute the transformation. 
%Relations between element types are derived from the relations of the JTL transformation, whereas constraints translate: a) the model patterns that must be matched by the model elements of the domain and b) pre- and post-conditions that must be obeyed. 
The transformation process logically consists of the following steps: 1) given the input (meta)models, the execution engine induces all the possible solution candidates according to the specified relations, and 2) the set of candidates is refined by means of constraints.

The application of the HSM2SM transformation (in Listing~\ref{lst:HSM2SMtransfJTL}) on the \emph{HSMm} model generates the corresponding \emph{SMm} model as depicted in the right part of Figure~\ref{fig:HSM2SMmodels}. Note that, by re-applying the transformation in the backward direction it is possible to obtain again the \emph{SMm} source model. The missing sub-states and the transitions involving them are restored by means of trace information.

Suppose that in a refinement step the designer needs to manually modify the generated target by the changes described in Section \ref{sec:sub-generatedmodels}. %(see $\Delta$ changes depicted in Figure~\ref{fig:HSM2SMmodels2}). 
%In particular, a) the new state \code{Printing} id added, b) the \code{print} transition  that associates \code{Active} state to the latter is added, and c) the source of the  \code{done} transition is modified from the \code{Active} state to the \code{Printing} state. 
The target model including such changes (\emph{SMm'}) is shown in the left part of the Figure \ref{fig:HSM2SMmodels2}. %If the transformation HSM2SM is applied on it, we expect changes to be propagated on the source model. However, 
Due to the incompleteness of the model transformation, 
%target changes may be propagated in a number of different ways, thus making the application of the reverse transformation to propose more solutions. The generated sources, namely \emph{HSMm'\_1}/\emph{2}/\emph{3}/\emph{4} can be inspected through Figure \ref{fig:HSM2SMmodels2}. 
%As previously said, 
the transition can be equally targeted to each one of the nested states within \code{Active} as well as to the super state itself (see the properties \emph{HSMm'\_1}/\emph{2}/\emph{3}/\emph{4} in Figure \ref{fig:HSM2SMmodels2}). For example, as visible in the property of the transition, \emph{HSMm'\_1} represents the case in which the transition is targeted to the composite state \code{Active}. 

  \begin{figure*}[htb]
    \center
     \includegraphics[width=12cm]{figures/xmi_c_d-new.jpg}
      \vspace{-0.3cm}
     \caption{The modified SM model and the correspondent HSM models}
      \vspace{-0.5cm}
       \label{fig:HSM2SMmodels2}
  \end{figure*}
  
% %
Even in this case, if the transformation is applied on one of the derived \emph{HSMm'} models, the appropriate \emph{SMm'} models including all the changes are generated. However, this time the target will preserve information about the chosen \emph{HSMm'} source model, thus causing future applications of the backward transformation to generate only \emph{HSMm'}.

With regard to the performances of our approach, the time required to execute each transformation in the illustrated case study is more than acceptable since always took less than one second. In the general case, when there are a lot of target alternative models the overall performance of the approach may degrade. 
Designers dealing with models containing uncertainty need to be supported with suitable mechanism and tools in order to avoid effect of having multiple design alternatives. 

%\begin{figure*}[htb]
%  \center
%   \includegraphics[width=13cm]{figures/xmi_c_d-new.jpg}
%    %%\vspace{-0.3cm}
%   \caption{The modified SM model and the correspondent HSM models}
%    %%\vspace{-0.5cm}
%     \label{fig:HSM2SMmodels2}
%\end{figure*}


 


